structure LCoqize = (*Coqize in low level*)
struct 
  structure Asm = Assem
  structure A = Assert
  (* added by lge 2006.05.14 --begin *)
  structure P = Proof
  structure E = ErrorMsg
  (* added by lge 2006.05.14 --end *)
  fun nullemit str:string = str  
  
  fun pr_st emit st = 
      let fun pr A.Rf = ("R",1)
	    | pr A.Hp = ("H",2)
	    | pr (A.Upd(st1,e0,e1)) = 
(*	      let val str_st1 = pr(st1)
		  val str_e0 = pr_exp nullemit e0
		  val str_e1 = pr_exp nullemit e1
	      in (print("need more work in update node");
		  "Upd("^str_st1^", "^str_e0^", "^str_e1^")")
	      end*)
	      let val str_st1 = pr(st1)
		  val str_e0 = pr_exp nullemit e0
		  val str_e1 = pr_exp nullemit e1
	      in ((fn 1 => "(updateR "^(#1 str_st1)^" "^str_e0^" "^str_e1^")"
		   | 2 => "(hw "^(#1 str_st1)^" "^str_e0^" "^str_e1^")"
		   | _ => (print("never happen\n");"")) (#2 str_st1), (#2 str_st1))
	      end 
      in pr(st)
      end

  and pr_exp emit e = 
      let fun pr (A.IntNum(i)) = 
	      if(i<0)
	      then ("(-"^Int.toString(Int.abs(i))^")")
	      else Int.toString(i)
	    | pr (A.Addr(ad)) = 
	      if(ad<0)
	      then ("(-"^Int.toString(Int.abs(ad))^")")
	      else Int.toString(ad)
	    | pr (A.Plus(e0,e1)) = 
	      let val str_e0 = pr_exp nullemit e0
		  val str_e1 = pr_exp nullemit e1
	      in "("^str_e0^"+"^str_e1^")"
	      end 
	    | pr (A.Minus(e0,e1)) = 
	      let val str_e0 = pr_exp nullemit e0
		  val str_e1 = pr_exp nullemit e1
	      in "("^str_e0^"-"^str_e1^")"
	      end 
	    | pr (A.Times(e0,e1)) = 
	      let val str_e0 = pr_exp nullemit e0
		  val str_e1 = pr_exp nullemit e1
	      in str_e0^"*"^str_e1
	      end 
	    | pr (A.Sel(st0,e0)) = 
(*	      let val str_st0 = pr_st nullemit st0
		  val str_e0 = pr_exp nullemit e0
	      in str_st0^"["^str_e0^"]"
	      end*)
	      let val str_st0 = pr_st nullemit st0
		  val str_e0 = pr_exp nullemit e0
	      in (fn 1 => "(lookupR "^(#1 str_st0)^" "^str_e0^")"
		   | 2 => "(hr "^(#1 str_st0)^" "^str_e0^")"
		   | _ => (print("never happen\n");"")) (#2 str_st0)
	      end
	    | pr A.Eax = "eax"
	    | pr A.Ebx = "ebx"
	    | pr A.Ecx = "ecx"
	    | pr A.Edx = "edx"
	    | pr A.Esi = "esi"
	    | pr A.Edi = "edi"
	    | pr A.Esp = "esp"
	    | pr A.Ebp = "ebp"
	    | pr _ = ""
      in emit (pr e)
      end
  
  fun pr_prop emit pp = 
      let fun pr A.True = "True"
	    | pr (A.Imply(p0,p1)) = 
	      let val str_p0 = pr_prop nullemit p0
		  val str_p1 = pr_prop nullemit p1
	      in str_p0^"->"^str_p1
	      end
	    | pr (A.Not(p0)) = 
	      let val str_p0 = pr_prop nullemit p0
	      in "(~"^str_p0^")"
	      end
	    | pr (A.And(p0,p1)) = 
	      let val str_p0 = pr_prop nullemit p0
		  val str_p1 = pr_prop nullemit p1
	      in "("^str_p0^")/\\("^str_p1^")"
	      end
	    | pr (A.Or(p0,p1)) = 
	      let val str_p0 = pr_prop nullemit p0
		  val str_p1 = pr_prop nullemit p1
	      in "("^str_p0^")\\/("^str_p1^")"
	      end
	    | pr (A.Gt(e0,e1)) = 
	      let val str_e0 = pr_exp nullemit e0
		  val str_e1 = pr_exp nullemit e1
	      in "("^str_e0^")>("^str_e1^")"
	      end
	    | pr (A.Ge(e0,e1)) = 
	      let val str_e0 = pr_exp nullemit e0
		  val str_e1 = pr_exp nullemit e1
	      in "("^str_e0^")>=("^str_e1^")"	      
	      end
	    | pr (A.Lt(e0,e1)) = 
	      let val str_e0 = pr_exp nullemit e0
		  val str_e1 = pr_exp nullemit e1
	      in "("^str_e0^")<("^str_e1^")"	      
	      end
	    | pr (A.Le(e0,e1)) = 
	      let val str_e0 = pr_exp nullemit e0
		  val str_e1 = pr_exp nullemit e1
	      in "("^str_e0^")<=("^str_e1^")"	      
	      end
	    | pr (A.Eq(e0,e1)) = 
	      let val str_e0 = pr_exp nullemit e0
		  val str_e1 = pr_exp nullemit e1
	      in "("^str_e0^")=("^str_e1^")"	      
	      end
	    | pr (A.Ne(e0,e1)) = 
	      let val str_e0 = pr_exp nullemit e0
		  val str_e1 = pr_exp nullemit e1
	      in "("^str_e0^")<>("^str_e1^")"	      
	      end
      in emit (pr pp)
      end

  (* added by lge 2006.5.14 --begin *)
  fun pr_atype emit at = 
      let fun pr (P.Prop(p)) = pr_prop emit p
            | pr (P.Stype(st)) = (raise Fail "WIP, will never go this way!"; "")
      in  emit (pr at)
      end 

  fun pr_pterm emit pt =
      let fun pr (P.Func((id, atype), pterm)) =
              let val ptype = pr_atype emit atype
                  val ppterm = pr_pterm emit pterm
              in  "fun ("^id^":"^ptype^") =>"^ppterm
              end
            | pr (P.Apply(pterm1, pterm2)) =
              let val ppterm1 = pr_pterm emit pterm1
                  val ppterm2 = pr_pterm emit pterm2
              in  "(" ^ ppterm1 ^ ") (" ^ ppterm2 ^ ")"
              end
            | pr (P.ID(s)) = s
            | pr (P.Exp(e)) = pr_exp emit e
      in emit (pr pt)
      end
  (* added by lge 2006.5.14 --end *)

  (* assertion to Coq format*)
  fun asst2coq' emit (label, bkasst) = 
      let val label' = 
	      (fn (#".") => (String.substring(label,1,
					      ((String.size label)-1)))
		| _ => label) (String.sub(label, 0))
	  val state = (A.Rf,A.Hp)
	  val prop = bkasst state
	  val str' = pr_prop nullemit prop
	  val str = "Lemma Asst_"^label'^": forall (R:rfile) (H:heap),"
		    ^str'^".\n"
      in emit str
      end 
  
  fun asst2coq bkinf = asst2coq' nullemit bkinf

  (* added by lge 2006.5.14 --begin *)
  (* assertion to Coq format*)
  fun asst2coq2' emit (label, bkasst, pterm) = 
      let val label' = 
	      (fn (#".") => (String.substring(label,1,
					      ((String.size label)-1)))
		| _ => label) (String.sub(label, 0))
	  val state = (A.Rf,A.Hp)
	  val prop = bkasst state
	  val str' = pr_prop nullemit prop
	  val str = "Lemma Asst_"^label'^": forall (R:rfile) (H:heap),"
		    ^str'^".\n"
          val term = pterm state
          val pstr' = pr_pterm nullemit term
          val pstr = "Proof.\n"^
                     "exact(\n"^
                     "fun (R:rfile)=> ( fun (H:heap) => ("^ pstr'^"))\n"^
                     ").\n"^
                     "Qed.\n"
          val str_pstr = str ^ pstr
      in emit str_pstr
      end 
  
  fun asst2coq2 bkinf = asst2coq2' nullemit bkinf

  fun coqhead () = "Require Export asm.\n"^
                   "Require Import ZArith.\n"^
                   "Open Scope Z_scope.\n\n"
  (* added by lge 2006.5.14 --end *)

  (* forward to Coq format*)
  fun fw2coq isdata spec instr = 
      (fn (Asm.Label (l,_)) => 
	  if isdata
	  then ""
	  else let val asst = A.getspec l spec 
	       in case (!asst)
		   of NONE => ""
		    | SOME a => asst2coq(l,a)
	       end
	| _ => "") instr

end
